debian/shuffle-boot-files: Handle boot/xen as well as boot/xen.gz
authorIan Jackson <iwj@amdahl.debian.org>
Fri, 12 Oct 2018 15:36:18 +0000 (15:36 +0000)
committerIan Jackson <ian.jackson@citrix.com>
Mon, 15 Oct 2018 11:09:03 +0000 (12:09 +0100)
commitf7d5e27b185bcd20a157d221d7928c5860134e8e
tree6388a4a1a4a5a1fc8501eb6b05835ca34fd270c8
parent441555179c58b96bcd97a12a87851a08a26af372
debian/shuffle-boot-files: Handle boot/xen as well as boot/xen.gz

On arm64, at least, the main file is boot/xen, not boot/xen.gz.

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
debian/shuffle-boot-files